T:Type, L:T List, i:(||L||-1), a, b:T.
a before b  swap(L;i;i+1)  a before b  L  a = L[i+1] & b = L[i] 

latex

Definitions	t  T, x:A. B(x), L1  L2, {T}, P  Q, (i, j), ||as||, P  Q, False, A, P & Q, AB, i  j < k, {i..j}, l[i], Prop, Dec(P), SQType(T), , hd(l), i<j, ij, tl(l), swap(L;i;j), ij, t  ...$L, P  Q, P  Q, x:A. B(x), x before y  l, b, b, , Unit, if b t else f fi, i=j, S  T, S  T
Lemmas	increasing implies, bool wf, ifthenelse wf, eq int wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, bnot wf, assert wf, not wf, l before wf, swap length, swap select, length nil, length cons, non neg length, swap wf, flip wf, length wf1, decidable lt, le wf, int seg wf, sublist pair, select wf, sublist wf